@$i$: $x$:$T$ initially $x$ = $v$($j$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ $x$ : $T$ initially $x$ = $v$ else  fi